package org.xteam.sled.model;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpPC;
import org.xteam.sled.semantic.exp.ExpRewriter;
import org.xteam.sled.semantic.exp.ExpTrue;

public abstract class BaseDisjunct<T extends ISequence> implements IDisjunct {
	
	protected String name;
	protected Set<Exp> conditions = new HashSet<Exp>();
	protected T sequence;
	
	public BaseDisjunct(String name, Set<Exp> conditions, T seq) {
		this.name = name;
		this.conditions = conditions;
		this.sequence = seq;
	}
	
	public String name() {
		return name;
	}
	
	@Override
	public void setName(String name) {
		this.name = name;
	}
	
	@Override
	public IDisjunct nameUnnamed(String newName) {
		if (name != null)
			return this;
		return createDisjunct(newName, new HashSet<Exp>(conditions), sequence);
	}

	@Override
	public IDisjunct subst(ExpRewriter subs) {
		Set<Exp> n = new HashSet<Exp>();
		for (Exp e : conditions) {
			Exp ee = subs.rewrite(e);
			if (! (ee.isConst() && (ee instanceof ExpTrue))) {
				n.add(ee);
			}
		}
		return createDisjunct(name, n, sequence.subst(subs));
	}
	
	@Override
	public Set<Exp> getConditions() {
		return conditions;
	}
	
	public boolean hasConditions() {
		return conditions.size() > 0;
	}
	
	public T getSequence() {
		return sequence;
	}
	
	@Override
	public boolean isContradictory() {
		return sequence.isContradictory();
	}
	
	@Override
	public boolean isFieldBinding() {
		return sequence.isFieldBinding();
	}
	
	@Override
	public void addConditions(List<Exp> constraints) {
		conditions.addAll(constraints);
	}
	
	protected abstract BaseDisjunct<T> createDisjunct(String name, Set<Exp> conds, ISequence seq);
	
	@Override
	public IDisjunct and(IDisjunct o) {
		BaseDisjunct<T> other = (BaseDisjunct<T>) o;
		int l1 = sequence.bitLength();
		int l2 = other.sequence.bitLength();
		int longest = Math.max(l1, l2);
		int pos1 = 0, pos2 = 0;
		ISequence newSeq = null;
		if ((sequence.hasPrefix() || other.sequence.hasPrefix())) {
			if (sequence.hasSuffix() || other.sequence.hasSuffix())
				throw new RuntimeException("Illegal conjunction; dots on both left and right");
			pos1 = longest - l1;
			pos1 = longest - l2;
			newSeq = sequence.mergeRight(other.getSequence());
		} else {
			newSeq = sequence.mergeLeft(other.getSequence());
		}
		Set<Exp> newConds = new HashSet<Exp>();
		addToPC(pos1, conditions, newConds);
		addToPC(pos2, other.conditions, newConds);
		return createDisjunct(null, newConds, newSeq);
	}
	
	@Override
	public IDisjunct seq(IDisjunct o) {
		BaseDisjunct<T> other = (BaseDisjunct<T>) o;
		if (sequence.hasSuffix() && allLocBindings(other.sequence.getElements()))
			throw new RuntimeException("illegal concatenation `... ; L:'");
		if (other.sequence.hasPrefix() && allLocBindings(sequence.getElements()))
			throw new RuntimeException("illegal concatenation `L: ...'");
		int k = sequence.bitLength();
		Set<Exp> newConds = new HashSet<Exp>();
		newConds.addAll(conditions);
		addToPC(k, other.conditions, newConds);
		List<ISequent> newElements = new ArrayList<ISequent>(getSequence().getElements());
		for (ISequent element : other.getSequence().getElements()) {
			newElements.add(element.subs(new PCSubstitute(k)));
		}
		ISequence newSeq = sequence.createSequence(getSequence().hasPrefix(), other.getSequence().hasSuffix(), newElements);
		return createDisjunct(null, newConds, newSeq);
	}
	
	@Override
	public IDisjunct postDots() {
		return createDisjunct(name, conditions, sequence.postDots());
	}
	
	@Override
	public IDisjunct preDots() {
		return createDisjunct(name, conditions, sequence.preDots());
	}
	
	private boolean allLocBindings(List<ISequent> elements) {
		for (ISequent element : elements) {
			if (! element.isLabel())
				return false;
		}
		return false;
	}
	
	private void addToPC (int pos, Set<Exp> conds, Set<Exp> result) {
		for (Exp e : conds) {
			result.add(new PCSubstitute(pos).rewrite(e));
		}
	}

	public static class PCSubstitute extends ExpRewriter {

		private Exp exp;

		public PCSubstitute(int bits) {
			this.exp = PatternUtils.addBitsToPC(bits);
		}

		public void visitPC(ExpPC expPC) {
			stack.push(exp);
		}
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		if (name != null)
			buffer.append(name).append("=");
		if (conditions.size() > 0) {
			buffer.append("{");
			boolean isFirst = true;
			for (Exp e : conditions) {
				if (! isFirst)
					buffer.append(", ");
				buffer.append(e);
				isFirst = false;
			}
			buffer.append("}");
		}
		buffer.append(sequence.toString());
		return buffer.toString();
	}
	
}
